i:Id, ds:x:Id fp Type, da:k:Knd fp Type, snd:msg-spec(ds;da).
msg-spec-loc-decl(snd;i;da)  msg-spec-loc(snd;i) 

latex

Definitions

IdLnk, t  T, x:A. B(x), msg-spec-links(snd), (x  l), source(l), <a,b>, Id, s = t, P  Q, x:AB(x), msg-spec-loc(snd;i), msg-spec-loc-decl(snd;i;da), Type, x. t(x), a:A fp B(a), Knd, msg-spec(ds;da), Top, 2of(t), x.A(x), fpf-domain(f), x:AB(x), 1of(t), msg-item(ds;da;k;l), type List, Atom$n, x:A. B(x), b, P & Q, P  Q, {T}, SQType(T), Prop, s ~ t, IdLnkDeq, KindDeq, product-deq(A;B;a;b), P  Q, left+right

Lemmas

member-fpf-domain, product-deq wf, Kind-deq wf, idlnk-deq wf, IdLnk sq, fpf-trivial-subtype-top, msg-item wf, pi1 wf, top wf, member map, fpf-domain wf, pi2 wf, msg-spec-loc-decl wf, msg-spec wf, Knd wf, fpf wf, Id wf, l member wf, msg-spec-links wf, IdLnk wf